Nuprl Definition : name-case
11,40
postcript
pdf
name-case(
n
;
i
,
k
.
A
(
i
;
k
);
j
,
x
.
B
(
j
;
x
))
== case
n
of inl(
ik
) => let
i
,
k
:LocKnd =
ik
in
A
(
i
;
k
) | inr(
p
) => let
j
,
x
=
p
in
B
(
j
;
x
)
latex
Definitions
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
let
i
,
k
:LocKnd =
ik
in
P
(
i
;
k
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
FDL editor aliases
name-case
origin